T:Type, X:MaInterface(T + Top), es:ES.
ma-interface-consistent(es;X)
 ([[ma-interface-left(X)]] = es-interface-left([[X]])  AbsInterface(T)) 

latex

Definitions	Type, MaInterface(T), ES, ma-interface-consistent(es;X), <a, b>, ma-interface-left(X), P  Q, P & Q, x:A  B(x), s = t, P  Q, x:AB(x), AbsInterface(A), es-interface-left(X), t  T, [[X]], left + right, Top, x:A. B(x), P  Q
Lemmas	ma-abs-interface wf, es-interface-left wf, es-interface wf, ma-abs-interface-compose